Nuprl Lemma : world_wf
0,22
postcript
pdf
world{i:l}
Type{i'}
latex
Definitions
Top
,
t
T
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
w-automaton(
T
;
TA
;
M
)
,
Id
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
mlnk(
m
)
,
source(
l
)
,
s
=
t
,
Msg(
M
)
,
{
x
:
A
|
B
(
x
) }
,
type
List
,
,
Type
,
w-action-dec(
TA
;
M
;
i
)
,
Action(
dec
)
,
IdLnk
,
World
Lemmas
IdLnk
wf
,
action
wf
,
w-action-dec
wf
,
nat
wf
,
Msg
wf
,
lsrc
wf
,
mlnk
wf
,
Id
wf
,
w-automaton
wf
,
top
wf
origin
T, f(a), 
x:A. B(x), w-automaton(T;TA;M), Id, x:A
B(x), x:A
B(x), mlnk(m), source(l), s = t, Msg(M), {x:A| B(x) }, type List, 
, Type, w-action-dec(TA;M;i), Action(dec), IdLnk, World